A:Type, eq:EqDecider(A), B:(AType), f:a:A fp B(a).
(0 < ||fpf-domain(f)||)
 (g:a:A fp B(a)
 (a:A
 (b:B(a)
 ((f  g  a : b & g  a : b  f
 (& (a':A. (a'  dom(g))  ((a' = a)))
 (& (||fpf-domain(g)|| < ||fpf-domain(f)||))) 

latex

Definitions

s = t, , t  T, x:A. B(x), A, x(s), ||as||, a < b, a:A fp B(a), Top, x:AB(x), Void, P  Q, False, f  g, P & Q, x:A  B(x), x:A. B(x), Type, f  g, P  Q, P  Q, (x  l), P  Q, n+m, left + right, i  j , type List, Dec(P), EqDecider(T), fpf-domain(f), hd(l), f(x), x  dom(f), b, eqof(d), f(a), b, x. t(x), <a, b>, f || g, if b then t else f fi , increasing(f;k), L1  L2, x : v, A c B, , {T}, SQType(T), s ~ t, , {x:A| B(x)} , x:A.B(x), x.A(x), , A  B

Lemmas

member-fpf-domain, length sublist, decidable int equal, proper sublist length, fpf-single wf, fpf-compatible-single2, fpf-compatible-symmetry, fpf-compatible-single-iff, fpf-ap wf, subtype rel self, fpf-join-dom, fpf-join-ap-sq, bool cases, eqtt to assert, bool sq, eqff to assert, fpf-single-dom-sq, not functionality wrt iff, assert of bnot, fpf-sub weakening, fpf-sub transitivity, fpf-join-sub, fpf-split, decidable assert, iff transitivity, assert of bor, or functionality wrt iff, assert-deq-member, deq property, fpf-join wf, fpf-sub wf, length wf1, fpf-domain wf, assert wf, fpf-dom wf, fpf-trivial-subtype-top, not wf